Generative Type Abstraction and Type-level Computation